Inference at * 1 3 1 0 2 3 
Iof proof for Lemma fincr wf:



1. P : 
2. j:. (k:. (k < j)  (P(k)))  (P(j))
3. n : 
4. (n < (n+1))  (P(n))
  P(n) 

latex

 by (D (-1)) 

latex

 1: .....antecedent..... NILNIL

 1: 3. n : 
 1:   n < (n+1)
 2: 

 2: 4. P(n)
 2:   P(n)
 .

Definitions

#$n, n+m, f(a), a < b, x:A. B(x), , , x:AB(x), P  Q